using System;
using Microsoft.Pex.Framework;
using Covana.ProblemExtractor;
using Microsoft.Pex.Framework.Settings;

namespace Benchmarks
{
    public static class LoopClass
    {
        public static void BubbleSort(int[] number,int[] k)
        {
            for (int i = 0; i < number.Length - 1; i++)
            {
                //for (int j = 0; j < number.Length - i - 1; j++)
                //{
                //    if (number[j] > number[j + 1])
                //    {
                //        int temp = number[j];
                //        number[j] = number[j + 1];
                //        number[j + 1] = temp;
                //    }
                //}
                //if (number[i] > number[i+1])
                //{
                //    int temp = number[i];
                //    number[i] = number[i + 1];
                //    number[i + 1] = temp;
                //}
            }

            if (number.Length > 1000)
            {
                throw new Exception("bug");
            }
        }

        public static void MoveMaxToTop(int[] number)
        {
            for (int i = 0; i < number.Length - 1; i++)
            {
                if (number[i] > number[i + 1])
                {
                    int temp = number[i];
                    number[i] = number[i + 1];
                    number[i + 1] = temp;
                }
            }

            if (number.Length > 5000)
            {
                throw new Exception("bug");
            }
        }
    }

    //[PexClass(typeof(LoopClass), TestEmissionFilter = PexTestEmissionFilter.All)]
    [PexClass(typeof(LoopClass))]
    [SearchFrontierDepthFirstAttribute]
    [BoundaryProblemObserver]
    public partial class LoopTest
    {
        [PexMethod]
        public int[] TestLoop(int[] n,int[] k)
        {
            //            PexAssume.IsTrue(n.Length >= 4999);
//            PexAssume.IsTrue(n.Length > 1000);
            LoopClass.BubbleSort(n,k);
            PexObserve.ValueForViewing("pc: ", PexSymbolicValue.GetPathConditionString());
            return n;
        }

        [PexMethod(MaxConditions = 10000, MaxBranches = 20000, MaxRunsWithoutNewTests = 10000)]
        public int[] TestLoop2(int[] n)
        {
//            PexAssume.IsTrue(n.Length >= 5000);
            LoopClass.MoveMaxToTop(n);
            return n;
        }
    }
}